Section: New Results

Run-Time Enforcement Using Büchi Games

Participants : Matthieu Renard [LaBRI] , Antoine Rollet [LaBRI] , Yliès Falcone.

In this work, we leverage Büchi games for the run-time enforcement of regular properties with uncontrollable events. Run-Time enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modeled by an automaton. We revisit run-time enforcement with uncontrollable events and propose a framework where we model the run-time enforcement problem as a Büchi game and synthesize sound, compliant, and optimal enforcement mechanisms as strategies. We present algorithms and a tool implementing enforcement mechanisms.We reduce the complexity of the computations performed by enforcement mechanisms at run-time by pre-computing the decisions of enforcement mechanisms ahead of time.

This work has been presented at the 24th ACM/SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017 [23].